r:Rng, e:|r|. (e r 0) = 1  |r| 

latex

Up	rings 1
Definitions of Statement	Rng, rxmn, e r n
Definitions	t  T, x:A. B(x), t.2, t.1, rxmn, e, |g|, e r n
Lemmas	rng wf, mul mon of rng wf c, mon nat op zero